#pragma once

/**********************************************************
oxsat - portable sat solver for windows and unix
Copyright (C) 2017  tj bandrowsky

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
*/

#include <vector>
#include <list>
#include "constants.h"
#include "clause.h"
#include "decision.h"
#include "istrategy.h"
#include "problem_variable.h"
#include "conflict.h"
#include <fstream>

//#define REALLY_LOUD

namespace solver
{
	class problem_solver
	{
	public:
		int max_conflict_variables;
		std::function<void(const char *message)> progress_func;
		int index;
		std::string problem_name;
		std::vector<problem_variable> variables;
		std::vector<pdecision> decisions;
		std::vector<pproduction> productions;
		decision_string_collection production_index;
		std::string comments;
		decision_string solution;
		bool verbose;
		bool fast_expand;
		decision_string picked_variables;

		problem_solver() : max_conflict_variables(32)
		{
			clear();
		}

		~problem_solver()
		{
			clear();
		}

		void clear()
		{
			verbose = false;
			fast_expand = true;
			srand(0);
			index = 0;
			solution.clear();
			problem_name.clear();
			variables.clear();
			comments.clear();
			for (int i = 0; i < decisions.size(); i++)
			{
				if (decisions[i]) {
					delete decisions[i];
					decisions[i] = nullptr;
				}
			}
			decisions.clear();
			for (int i = 0; i < productions.size(); i++)
			{
				if (productions[i]) {
					delete productions[i];
					productions[i] = nullptr;
				}
			}
			productions.clear();
		}

		class guess_literal_result
		{
		public:
			bool success;
			bool complete;
			bool conflict;
			literal guess;
			decision *dec;

			guess_literal_result() : success(false), complete(false), conflict(false), dec(nullptr)
			{

			}
		};

		class apply_literal_result
		{
		public:
			bool unsatisfiable;
			bool unsolveable;
			bool conflicted_guess;
			std::string failreason;

			apply_literal_result() : unsolveable(false), conflicted_guess(false), unsatisfiable(false)
			{

			}
		};

		class step_result
		{
		public:
			bool finished;
			bool solved;
			bool unsolveable;
			bool unsatisfiable;
			bool validated;
			std::string reason;

			step_result() : finished(false), solved(false), unsolveable(false), unsatisfiable(false), validated(false)
			{

			}

			apply_literal_result apply_result;
			guess_literal_result guess_result;
		};

		step_result last_step_result;

		step_result step(solver::istrategy& solver_strategy)
		{
			step_result result;

			result.guess_result = guess_literal();

			if (result.guess_result.complete)
			{
				result.finished = true;
				if (result.guess_result.conflict)
				{
					result.unsatisfiable = true;
					result.reason = "All the previous variables were eliminated from ";
					result.reason += to_string(result.guess_result.dec);
				}
				else
				{
					result.solved = true;
					result.reason = to_string(solution, " ");
					result.validated = apply_solution(solver_strategy);
				}
				last_step_result = result;

				return result;
			}
			else
			{
				result.apply_result = apply_literal(result.guess_result.guess, result.guess_result.conflict);
				if (
					result.apply_result.unsolveable ||
					result.apply_result.unsatisfiable
					)
				{
					result.finished = true;
					result.reason = result.apply_result.failreason;
					result.unsatisfiable = result.apply_result.unsatisfiable;
					result.unsolveable = result.apply_result.unsolveable;
				}
			}
			last_step_result = result;
			return result;
		}

		bool solve(solver::istrategy& solver_strategy)
		{
			step_result result;
			do
			{
				result = step(solver_strategy);
			} while (!result.finished);

			if (!result.solved)
			{
				solution.clear();
			}
			return result.solved;
		}

		std::string to_string(solver::production *cur_prod)
		{
			std::string implication_text = "";

			if (cur_prod->product.ref == -1)
			{
				implication_text = "Conflict <- ";
			}
			else
			{
				auto& v = variables[cur_prod->product.ref];
				if (cur_prod->product.val == 0)
				{
					implication_text += "!";
				}
				implication_text += std::to_string(v.name);
				implication_text += " <- ";
			}

			implication_text += to_string(cur_prod->match, " ");

			return implication_text;
		}

		std::string to_string(solver::pdecision dec)
		{
			std::string text;

			text = "(";
			bool written = false;
			size_t ds = dec->literals.size();
			for (int i = 0; i < ds; i++)
			{
				auto& vs = dec->literals[i];

				if (written) {
					text += " | ";
				}
				auto& v = variables[vs.ref];

				if (vs.val == 0) {
					text += "!";
					text += std::to_string(v.name);
				}
				else
				{
					text += std::to_string(v.name);
				}
				written = true;
			}
			text += ") at line ";
			text += std::to_string(dec->line_number);

			return text;
		}

		std::string to_string(solver::decision_string& dstr, const char *delimiter = nullptr)
		{
			std::string x = "";
			if (dstr.is_c_str) {
				auto dcdestn = dstr.first();
				while (dcdestn != nullptr)
				{
					auto& dcdest = dcdestn->value;
					if (!dcdest.val)
					{
						x += "!";
					}
					std::string temp(1, (char)variables[dcdest.ref].name);
					x += temp;
					if (delimiter != nullptr) {
						x += delimiter;
					}
					dcdestn = dstr.next(dcdestn);
				}
			}
			else {
				auto dcdestn = dstr.first();
				while (dcdestn != nullptr)
				{
					auto& dcdest = dcdestn->value;
					if (!dcdest.val)
					{
						x += "!";
					}

					x += std::to_string(variables[dcdest.ref].name);
					if (delimiter != nullptr) {
						x += delimiter;
					}
					dcdestn = dstr.next(dcdestn);
				}
			}
			return x;

		}


	private:

		bool apply_solution(solver::istrategy& solver_strategy)
		{
			bool solution_valid = true;
			size_t vc = variables.size();
			size_t ds = decisions.size();
			int i;
			int t;

			for (i = 0; i < ds; i++)
			{
				auto dec = decisions[i];
				dec->selected_literal = -1;
			}

			for (i = 0; i < vc; i++)
			{
				auto& v = variables[i];
				v.check_valid = true;
				v.value = -1;
			}

			auto dcdestn = solution.first();
			while (dcdestn != nullptr)
			{
				auto& ch = dcdestn->value;

				auto& v = variables[ch.ref];
				t = ch.val;

				if (v.check_valid && (v.value == -1 || v.value == t))
				{
					v.value = t;
				}
				else
				{
					v.check_valid = false;
					solution_valid = false;
					std::cout << "c variable " << v.name << " has conflicting assignments." << std::endl;
				}

				dcdestn = solution.next(dcdestn);
			}

			for (int j = 0; j < ds; j++)
			{
				auto dec = decisions[j];
				bool found_literal = false;
				for (int i = 0; i < dec->literals.size(); i++)
				{
					if (solution.exists_exact(dec->literals[i]))
					{
						found_literal = true;
						dec->selected_literal = i;
						break;
					}
				}
				if (!found_literal)
				{
					std::cout << "c decision " << to_string(dec) << " has no assignment." << std::endl;
					solution_valid = false;
				}
			}
			return solution_valid;
		}

		guess_literal_result guess_literal()
		{
			guess_literal_result result;

			char buff[256];
			if (verbose)
			{
				sprintf(buff, "%d lits", solution.size());
				write_console("");
				write_console(buff);
			}

			int nd = decisions.size();
			int icc = 0;

			do 
			{
				decision *dec = decisions[icc];
				int nds = dec->literals.size();
				result.dec = dec;
				result.guess.ref = -1;

				for (int j = 0; j < nds; j++)
				{
					auto lt = dec->literals[j];
					if (solution.exists_exact(lt))
					{
						goto next_clause;
					}
					else if (!solution.exists(lt))
					{
						result.guess = lt;
						multiconflict_iterator conflicts(max_conflict_variables);
						decision_string temp;
						temp = solution;
						temp.add(lt);
						if (get_conflicts(temp, conflicts, true) == 0) {
							return result;
						}
					}
				}

				if (result.guess.ref > -1)
				{
					result.conflict = true;
					return result;
				}

				// this should never happen because the conflict will be detected
				result.complete = true;
				return result;

			next_clause:
				icc++;
			} while (icc < nd);

			result.conflict = false;
			result.complete = true;
			return result;
		}

		int get_conflicts(decision_string& ds, multiconflict_iterator& conflicts, bool test)
		{
			std::list<literal_node *> found_conflict_strings;
			int conflicts_added = 0; 
			int current_dsize;
			decision_string temp = ds;
			
			do
			{
				current_dsize = ds.size();

#ifdef REALLY_LOUD
				if (verbose)
				{
					write_console("checking:", ds);
				}
#endif

				std::list<literal_node *> found_strings;
				production_index.find_strings(temp, found_strings);

				for (auto& nd : found_strings)
				{
					auto& prd = productions[nd->string_id];
					if (prd->product.ref > -1)
					{
						bool res = temp.add(prd->product);
					}
				}

			} while (current_dsize < ds.size());

			std::list<literal_node *> conflict_strings;
			production_index.find_strings(temp, conflict_strings);

			for (auto& nd : conflict_strings)
			{
				auto& prd = productions[nd->string_id];
				if (prd->product.ref == -1)
				{
					conflicts_added += conflicts.add(prd,test);
				}
			}

			if (!test)
			{
				ds = temp;
			}

			return conflicts_added;
		}

		class resolve_conflict_result {
		public:

			bool unresolvable;
			bool unsatisfiable;
			std::string reason;
			decision_string new_solution;
		};

		std::string get_fail_string(multiconflict_iterator& conflicts, std::list<pdecision>& failed_decisions)
		{
			std::string temp;
			std::list<conflict_mapping *> failed;
			conflicts.get_failed_conflicts(failed);
			for (auto cm : failed)
			{
				char buff[32];
				sprintf(buff, " %lld times.", cm->fail_count);
				std::string line = "c " + to_string(cm->match_prod);
				line += buff;
				line += " from ";
				if (cm->match_prod->source_clause)
				{
					line += to_string(cm->match_prod->source_clause);
				}
				else {
					line += " unreferenced literal";
				}
				line += "\n";
				temp += line;
			}
			temp += "\nc thus fails these";
			for (auto fd : failed_decisions)
			{
				temp += "\nc " + to_string(fd);
			}
			return temp;
		}

		bool find_failed_clauses(decision_string& solution, std::list<pdecision>& failed_clauses)
		{
			bool success = false;
			for (auto dec : decisions)
			{
				bool complete = true;
				for (auto l : dec->literals)
				{
					if (!solution.exists(l))
					{
						complete = false;
						break;
					}
				}
				if (complete)
				{
					failed_clauses.push_back(dec);
					success = true;
				}
			}
			return success;
		}

		void add_conflict(decision_string& conflict)
		{
			production *new_production = new production();
			new_production->match = conflict;
			new_production->product.ref = -1;
			new_production->product.ref = -1;
			new_production->stringid = production_index.add(conflict);
			new_production->source_clause = nullptr;
			productions.resize(new_production->stringid + 1);
			productions[new_production->stringid] = new_production;
		}

		resolve_conflict_result resolve_conflict_fail(multiconflict_iterator& conflicts)
		{
			char buff[256];
			resolve_conflict_result result;
			result.unsatisfiable = false;

			std::list<pdecision> failed;
			bool foundfail = find_failed_clauses(conflicts.last_result, failed);
			if (foundfail)
			{
				sprintf(buff, "%lld/ %lld examined. ", conflicts.get_conflict_idx(), conflicts.get_conflict_scale());
				result.reason = buff;
				result.unsatisfiable = true;
				result.unresolvable = true;
				result.reason += to_string(conflicts.last_result, " ") + " always conflicts\n" + get_fail_string(conflicts, failed);
			}
			return result;
		}

		resolve_conflict_result resolve_conflict(decision_string ds)
		{
			decision_string_collection heuristic;

			resolve_conflict_result result;
			result.unsatisfiable = false;
			result.unresolvable = false;
			result.reason = "Ok";

			int count = 0;
			char buff[256];
			decision_string temp;
			multiconflict_iterator conflicts( max_conflict_variables );
			conflicts.verbose = verbose;

			while (true)
			{
				big_int current_value;
				int conflict_count = -1;

				if (!get_conflicts(ds, conflicts, false))
				{
					result.new_solution = ds;
					return result;
				}

				if (verbose)
				{
					sprintf(buff, "Resolving %d, %lld", conflicts.size(), conflicts.get_conflict_scale());
					write_console(buff);
				}

				if (conflicts.size() > max_conflict_variables)
				{
					result.reason = "Too many conflict variables.";
					result.unresolvable = true;
					result.unsatisfiable = false;
					return result;
				}

				bool found_solution = conflicts.get_first(ds);
				if (verbose)
				{
					auto dec = conflicts.get_variables();
					write_console("Variables:", dec);
					write_console("Trial:", conflicts.last_result);
					for (auto& c : conflicts.conflicts)
					{
						std::string temp;
						temp = to_string(c->match_prod->match, " ");
						write_console(temp);
					}
				}

				if (!found_solution)
				{
					return resolve_conflict_fail(conflicts);
				}

			retry:
				temp = ds;
				// TODO: Experiment with this.  You should not have to have conflict chaining!!!!!
				conflicts.clear();
				int count = get_conflicts(temp, conflicts, true);
				if (!count)
				{
					if (verbose) {
						sprintf(buff, "Found %d conflicts:", count);
						write_console(buff, conflicts.last_result);
					}
					result.unresolvable = false;
					result.unsatisfiable = false;
					result.new_solution = temp;
					return result;
				}
				else 
				{
					if (count < conflict_count || conflict_count == -1 || fast_expand)
					{
						std::list<literal_node *> found_strings;
						if (!heuristic.find_strings(ds, found_strings))
						{
							conflict_count = count;
							current_value = conflicts.current_value;
							if (fast_expand) 
							{
								goto fast_expand_spot;
							}
						}
					}
					if (conflicts.get_next(ds))
					{
#ifdef REALLY_LOUD
						if (verbose)
						{
							sprintf(buff, "Trial %d conflicts:", count);
							write_console(buff, conflicts.last_result);
						}
#endif
						goto retry;
					}
				}

			fast_expand_spot:

				if (conflict_count > -1) 
				{
					if (verbose) {
						sprintf(buff, "Folding in %d more conflicts using:", conflict_count);
						write_console(buff, conflicts.last_result);
					}
					conflicts.current_value = current_value;
					conflicts.fold_values(ds);
					heuristic.add(ds);
				}
				else 
				{
					result.reason = "Unsatisfiable because everything we tried didn't work.";
					result.unresolvable = true;
					result.unsatisfiable = true;
					return result;
				}
			}

			result.reason = "Error of doom.";
			result.unresolvable = true;
			result.unsatisfiable = false;
			return result;
		}

		void write_console(const char * src)
		{
			std::string temp;
			temp = src;
			write_console(temp);
		}

		void write_console(const char *note, decision_string& src)
		{
			std::string temp;
			temp = note;
			temp += to_string(src, " ");
			write_console(temp);
		}

		void write_console(decision_string& src)
		{
			std::string temp;
			temp = to_string(src, " ");
			write_console(temp);
		}

		void write_console(std::string& src)
		{
			if (progress_func) 
			{
				progress_func(src.c_str());
			}
		}

		apply_literal_result apply_literal(literal guess, bool has_conflicts)
		{
			apply_literal_result result;

			bool decent_guess = solution.add(guess);
			if (!decent_guess)
			{
				result.unsolveable = true;
				result.failreason = "Internal consistency problem.";
				return result;
			}

			multiconflict_iterator conflicts( max_conflict_variables );

			if (has_conflicts)
			{
				auto resolve_result = resolve_conflict(solution);
				result.unsolveable = resolve_result.unresolvable;
				result.conflicted_guess = false;
				result.unsatisfiable = resolve_result.unsatisfiable;
				result.failreason = resolve_result.reason;
				if (!resolve_result.unresolvable)
				{
					solution = resolve_result.new_solution;
				}
			}
			else 
			{
				result.unsolveable = false;
				result.conflicted_guess = false;
				result.unsatisfiable = false;
			}

			return result;
		}

	};
}
